A Tableau Based Decision Procedure for an Expressive \ud Fragment of Hybrid Logic with Binders, Converse and Global Modalities

摘要

In this paper we provide the first (as far as we know) direct calculus\uddeciding satisfiability of formulae in negation normal form in the\udfragment of FHL (full hybrid logic with the binder, including the\udglobal and converse modalities), where no occurrence of a universal\udoperator is in the scope of a binder. By means of a satisfiability\udpreserving translation of formulae, the calculus can be turned into a\udsatisfiability decision procedure for the fragment $FHL\setminus\Box\ud\binder\Box$, i.e. formulae in negation normal form where no\udoccurrence of the binder is both in the scope of and contains in its\udscope a universal operator.\ud\udThe calculus is based on tableaux and termination is achieved by means\udof a form of anywhere blocking with indirect blocking. Direct\udblocking is a relation between nodes in a tableau branch, holding\udwhenever the respective labels (formulae) are equal up to (a proper\udform of) nominal renaming. Indirect blocking is based on a partial\udorder on the nodes of a tableau branch, which arranges them into a\udtree-like structure.